#include <stdio.h>
#include <getopt.h>
#include <errno.h>
#include <stdlib.h>
#include <limits.h>


#define olog()  cout<<__FILE__<<":"<<__PRETTY_FUNCTION__<<":"<<__LINE__<<": "
#define elog()  cerr<<__FILE__<<":"<<__PRETTY_FUNCTION__<<":"<<__LINE__<<": "


#include "PDTGraphVisitor.h"
#include "PDTNumVar.h"
#include "PDTExpBoolBinNumDerived.h"
#include "PDTExpNumBinDerived.h"
#include "PDTProp.h"
#include "PDTCodeGraph.h"
#include "PDTNumConst.h"
#include "PDTAssign.h"
#include "PDTBoolVar.h"
#include "PDTExpBoolBinBoolDerived.h"
#include "PDTSetOp.h"
#include "PDTIfElse.h"
#include "PDTAssert.h"
#include "PDTListOfStatements.h"
#include "PDTType.h"
#include "PDTSetVar.h"
#include "PDTQuantifier.h"
#include "PDTBoolConst.h"
#include "PDTNeg.h"
#include "PDTNot.h"
#include "PDTWhile.h"

#include "CGTranslate2SC.h"
#include "PDTZ3GraphVisitor.h"

long
cstringtolong(const char * str) 
{
    char * endptr = NULL;
    unsigned int base = 10;
    errno = 0;    /* To distinguish success/failure after call */
    long val = strtol(str, &endptr, base);
    /* Check for various possible errors */

    if ((errno == ERANGE && (val == LONG_MAX || val == LONG_MIN))
            || (errno != 0 && val == 0)) {
        perror("strtol");
        exit(EXIT_FAILURE);
    }
    if (endptr == str) {
        cerr << "cstringtolong: No digits were found" << endl;
        exit(EXIT_FAILURE);
    }

    if (*endptr != '\0')        /* Not necessarily an error... */
        cout << "cstringtolong: further characters after number: " <<  endptr << endl;
    return val;
}


void myTest()
{
	PDTCodeGraph CG;

	/*
	PDTNumConstInt seven(CG, 7);
	PDTNumConstInt twenty(CG, 20);
	PDTNumConstInt nine(CG, 9);
	PDTNeg neg(CG, seven);
	PDTAdd add(CG, twenty, neg);
	PDTSubt subt(CG, add, neg);
	PDTDiv div(CG, subt, add);
	PDTMod mod(CG, subt, add);
	PDTBoolConst trueConst(CG, true);
	PDTBoolConst falseConst(CG, false);
	PDTNot notT(CG, trueConst);
	PDTAnd andT(CG, trueConst, trueConst);
	PDTImplies implies(CG, trueConst, notT);
	PDTGreaterThanEqual greaterThanEqual(CG, seven, mod);
	PDTNumVar a(CG, "a");
	PDTAssign assign00(CG, a, div);
	a.eval(CG);
	assign00.eval(CG);
	a.eval(CG);

	cout<<endl;
	cout<<"WHILE TEST"<<endl;
	cout<<"=========="<<endl;

	//int i = 0;
	//int S = 0;
	//while (i<=10)
	//{
	//    S := S + i;
	//    i := i + 1;
	//}

	PDTNumConstInt zero(CG, 0);
	PDTNumConstInt one(CG, 1);
	PDTNumConstInt ten(CG, 10);


	PDTNumVar i(CG, "i");
	PDTNumVar s(CG, "s");
	PDTAssign assign1(CG, i, one);
	PDTAssign assign2(CG, s, zero);
	assign1.eval(CG);
	assign2.eval(CG);

	PDTAdd add1(CG, i, one);
	PDTAssign assign3(CG, i, add1);
	PDTAdd add2(CG, s, i);
	PDTAssign assign4(CG, s, add2);

	vector<PDTStatement*> whileList;
	whileList.push_back(&assign4);
	whileList.push_back(&assign3);


	PDTLessThanEqual lessThanEqual(CG, i, ten);

	PDTListOfStatements listWhile(CG, whileList);
	PDTWhile whileLoop(CG, lessThanEqual, listWhile);

	whileLoop.eval(CG);
	cout<<endl;
	cout<<"FinalResult: ";
	s.eval(CG);

	cout<<endl<<endl;

	cout<<endl;
	*/
	/*cout<<"SEQUENCE TEST - Averaging sequence elements"<<endl;
	cout<<"==========================================="<<endl;

	PDTNumConstInt zero(CG, 0);
	PDTNumConstInt one(CG, 1);
	PDTNumConstInt two(CG, 2);
	PDTNumConstInt three(CG, 3);
	PDTNumConstInt four(CG, 4);
	PDTNumConstInt five(CG, 5);
	PDTNumConstInt nine(CG, 9);
	PDTNumConstInt ten(CG, 10);
	PDTNumConstInt eleven(CG, 11);
	PDTNumConstInt twelve(CG, 12);
	PDTNumConstInt thirteen(CG, 13);

	PDTNumVar x(CG, "x");
	PDTIntRange seqRange(CG, "seqRange", zero, five);
	PDTSequence A(CG, "A", &PDTType::Int, &seqRange);
	PDTSequenceAccessNum atZero(CG, A, zero);
	PDTSequenceAccessNum atOne(CG, A, one);
	PDTSequenceAccessNum atTwo(CG, A, two);
	PDTSequenceAccessNum atThree(CG, A, three);
	PDTSequenceAccessNum atFour(CG, A, four);
	PDTAssign assign01(CG, atZero, nine);
	PDTAssign assign02(CG, atOne, ten);
	PDTAssign assign03(CG, atTwo, eleven);
	PDTAssign assign04(CG, atThree, twelve);
	PDTAssign assign05(CG, atFour, two);
	PDTAssign assign06(CG, atFour, thirteen);


	assign01.eval(CG);
	assign02.eval(CG);
	assign03.eval(CG);
	assign04.eval(CG);
	assign05.eval(CG);
	assign06.eval(CG);

	PDTNumVar i(CG, "i");
	PDTNumVar s(CG, "s");
	PDTAssign assign1(CG, i, zero);
	PDTAssign assign2(CG, s, zero);
	assign1.eval(CG);
	assign2.eval(CG);

	PDTAdd add1(CG, i, one);
	PDTAssign assign3(CG, i, add1);
	PDTSequenceAccessNum atI(CG, A, i);
	PDTAdd add2(CG, atI, s);
	PDTAssign assign4(CG, s, add2);

	vector<PDTStatement*> whileList;
	whileList.push_back(&assign4);
	whileList.push_back(&assign3);


	PDTLessThanEqual lessThanEqual(CG, i, four);

	PDTListOfStatements listWhile(CG, whileList);
	PDTWhile whileLoop(CG, lessThanEqual, listWhile);

	whileLoop.eval(CG);
	PDTDiv divide(CG, s, five);
	s.eval(CG);
	divide.eval(CG);
	string es;
	es = "He";
	PDTGreaterThan greater(CG, divide, s);
	PDTBoolVar booleanV(CG,"bvasdfarrr");
	PDTBoolConst boolTrue(CG, true);
	PDTBoolConst boolFalse(CG, false);
	PDTAssign assssss(CG, booleanV, boolFalse);
	assssss.eval(CG);

	PDTNot notnot(CG, booleanV);
	PDTAnd andand(CG, boolTrue, notnot);*/
}


void
test1()
{
  /*
   * int a, b, c;
   * bool expression e1 : a > b;
   * int expresseion: e2: b + c;
   * int expression: e4 = b - c;
   * if ( e1 ) {
   *   a := e2; -- a2
   *   c := 1;  -- a3
   * } else {
   * 	 a := e4; -- a4
   *   b := 1;  -- a5
   * }
   * a := 3;
   */
  PDTCodeGraph CG;
  PDTNumVar a(CG, "a");
  PDTNumVar b(CG, "b");
  PDTNumVar c(CG, "c");
  PDTNumConstInt one(CG, 1);
  PDTNumConstInt three(CG, 3);
	
one.eval(CG);

  PDTGreaterThan e1(CG, a, b);

  PDTAdd e2(CG, b, c);
  PDTAssign a2(CG, a, e2);
  PDTAssign a3(CG, c, one);

  vector<PDTStatement*> listIf;
  listIf.push_back(&a2);
  listIf.push_back(&a3);

  PDTSubt e4(CG, b, c);
  PDTAssign a4(CG, a, e4);
  PDTAssign a5(CG, b, one);

  vector<PDTStatement*> listElse;
  listElse.push_back(&a4);
  listElse.push_back(&a5);

  PDTListOfStatements ifList(CG, listIf);
  PDTListOfStatements elseList(CG, listElse);
  PDTIfElse ifElse(CG, e1, ifList, elseList);

  PDTAssign a6(CG, a, three);

  stringstream ss(stringstream::in | stringstream::out);
  a6.toString(ss);
  cout << ss.str() << endl;
}

void
test2()
{
  PDTCodeGraph CG;

  PDTNumVar x(CG, "x");
  PDTNumConstInt zero(CG, 0);
  PDTNumConstInt two(CG, 2);
  PDTMod rem(CG, x, two);
  PDTEqualNum exp(CG, rem, zero);
  vector<PDTVar*> vars;
  vars.push_back(&x);
  PDTForall c1(CG, vars, exp);
  PDTAssert a1(CG, c1);

  stringstream ss(stringstream::in | stringstream::out);
  a1.toString(ss);

  cout << ss.str() << endl;
}

void
test3()
{
#if 0
  while (Not ( ( ( bv = 1 ) And ( a <= ( -b) ) ) ))
    {
      a := (a + b)
      a := 2
      if ( Not ( ( ( bv = 1 ) And ( a <= ( -b) ) ) ) )
        {
          a := (a + b)
        }
      else
        {
          if ( ( a <= ( -b) ) )
            {
              a := (a + b)
            }
          else
            {
              a := 2
            }
        }
    }
#endif

  PDTCodeGraph CG;
  PDTNumVar a(CG, "a");

  PDTNumVar b(CG, "b");
  PDTBoolVar bv(CG, "bv");
  PDTNumConstInt const1(CG, 2);
  PDTBoolConst bc(CG, true);

  PDTAdd add1(CG, a, b);

  PDTAssign assign1(CG, a, add1);
  PDTAssign assign2(CG, a, const1);
  PDTNeg neg1(CG, b);
  PDTLessThanEqual less1(CG, a, neg1);
  PDTEqualBool equal1(CG, bv, bc);
  PDTAnd and1(CG, equal1, less1);
  PDTNot not1(CG, and1);

  PDTIfElse ifelse2(CG, less1, assign1, assign2);
  PDTIfElse ifelse(CG, not1, assign1, ifelse2);

  vector<PDTStatement*> slist;
  slist.push_back(&assign1);
  slist.push_back(&assign2);
  slist.push_back(&ifelse);
  //slist.push_back(&ifelse);

  PDTListOfStatements list(CG, slist);
  PDTWhile while1(CG, not1, list);

  stringstream ss;
  while1.toString(ss);
  cout << ss.str() << endl;

  PDTCG2SC transform(CG);
  transform.setVarBound("a", 64);
  transform.setVarBound("b", 16);
  transform.toBlif();
}

int
cg2scMain(int argc, char ** argv)
{
	cout<<endl;
	cout<< "My Test"<<endl;
	cout<< "======="<<endl;
	myTest();
  /*cout << "Test 1" << endl;
  test1();

  cout << "Test 2" << endl;
  test2();

  cout << "Test 3" << endl;
  test3();

  cout << "Done" << endl;
*/
  return 0;
}


class TryTraversal : public Traversal {public:
        virtual RetType pre(PDTIfElse & d) {
            olog() << endl;
            return Continue;}

        virtual RetType pre(PDTAssign & d) {
            olog() << endl;
            return Continue;}
};

extern PDTCodeGraph *
mini_main(const string & file);

extern int
specCheckMain(const string & file, const string & func, const string & spec);

extern int 
ABCMain(const std::string & inputFile, const std::string & funcName, unsigned int scalarBound, unsigned int arrayBound, bool abc_debug);

void
testMiniZ3(const string & file)  {
  PDTCodeGraph * cg = mini_main(file) ;
  PDTZ3Visitor z3Vst(*cg);
  z3Vst.check();
  delete cg;
}

void
testTraversal(const string & file)  {
  PDTCodeGraph * cg = mini_main(file) ;
  TryTraversal t;
  for (unsigned int i = 0; i < cg->nodes.size(); i++) {
      PDTNode * node = cg->nodes[i];
      if (node->getParents().size() == 0)
          node->traverseEx(t);
    }
  delete cg;
}

extern int checkSpecGUIMain(int argc, char ** argv,
        const string & inFile, const string & funcName, const string & specName);

int
main(int argc, char ** argv)
{
    string inputFile ="";
    string funcName ="";
    string specName = "";

    bool specCheck = false;
    bool abc = false;
    bool abc_debug = false;
    bool smt = false;
    bool gui = false;

    long verbosity = 7;
    int bound = 2;
    int array_bound = 0;

    typedef enum {
        RUN_SMT = 1, RUN_ABC= 2, ABC_DEBUG=3, ARRAY_BOUND=4
    } OPT_VALS;

    int option_index = 0;

    static struct option long_options[] = {
        {"file", 1, 0, 'i'},
        {"function", 1, 0, 'f'},
        {"spec", 1, 0, 's'},
        {"verbose", 1, 0, 'v'},
        {"check", 0, 0, 'c'},
        {"bound", 1, 0, 'b'}, // bound on variables

        {"smt", 0, 0, RUN_SMT},
        {"abc", 0, 0, RUN_ABC},
        {"debug-abc", 0, 0, ABC_DEBUG},
        {"array-bound", 1, 0, ARRAY_BOUND},
        {"gui", 0, 0, 'g'},
        {"help", 0, 0, 'h'},
        {0,0,0,0}
    };

    while(true) {
        int c = getopt_long (argc, argv, "i:f:s:v:cgh",
                long_options, &option_index);

        if (c == -1)
            break;

        switch(c) {
            case 'h': 
                cout << "    ' -h or --help' for this message." << endl;
                cout << "    ' -i or --file filename' to specify input file name." << endl;
                cout << "    ' -f or --function functionname' to specify function name." << endl;
                cout << "    ' -s or --spec specname' to specify specification name." << endl;
                cout << "    ' -v or --verbose number' to specify verbosity level." << endl;
                cout << "    ' -c or --check' to run specCheck." << endl;
                cout << "    ' -b or --bound bound_value' to specify the bound on the latches in sequential synthesis" << endl;
                cout << "    ' --array_bound bound_value' to specify the bound on the arrays in sequential synthesis" << endl;
                cout << "    ' --smt' to translate to smt and run z3 (not fully implemented)." << endl;
                cout << "    ' --abc' to translate to sequential circuit and run abc (not fully implemented)." << endl;
                cout << "    ' --debug-abc' to invoke abc debugging using PDTSimulate." << endl;
                cout << "    ' -g or --gui' to invoke gui interface (not fully implemented)." << endl;
                exit(0);
                break;
            case  'i':
                if (optarg == NULL) {
                    cerr << "-i or --file takes a file name argument" << endl;
                    exit(0);
                }
                inputFile = optarg;
                break;  
            case  'f':
                if (optarg == NULL) {
                    cerr << "-f or --function takes a function name argument" << endl;
                    exit(0);
                }
                funcName = optarg;
                break;  
            case  's':
                if (optarg == NULL) {
                    cerr << "-s or --spec takes a spec (pre,post, behavior tuple) name argument" << endl;
                    exit(0);
                }
                specName = optarg;
                break;  
            case  'v':
                if (optarg == NULL) {
                    cerr << "-v or --verbose takes a number that configures verbosity of log" << endl;
                    cerr << "  1: errors, 2: warnings, 4: messages, 8: logs, 16: debug" << endl;
                    cerr << "  example: 7 means 1+2+4; 31 means 1+2+4+8+16" << endl;
                    exit(0);
                }
                verbosity = cstringtolong(optarg);
                break;  
            case  'b':
                if (optarg == NULL) {
                    cerr << "-b or --bound takes an integer input value" << endl;
                    exit(0);
                }
                bound = atoi(optarg);
                break;
            case  'c':
                specCheck = true;;
                break;  
            case  RUN_SMT:
                smt = true;;
                break;  
            case  RUN_ABC:
                abc = true;;
                break;  
            case  ABC_DEBUG:
                abc_debug = true;;
                break;
            case ARRAY_BOUND:
                if (optarg == NULL) {
                    cerr << "--array_bound takes an integer input value" << endl;
                    exit(0);
                }
                array_bound = atoi(optarg);
                break;
            case  'g':
                gui = true;
                break;  
            default:
                break;
        }
    }


    if (gui) {
        checkSpecGUIMain(argc, argv, inputFile, funcName, specName);
        return 0;
    }

    if (inputFile.empty()) {
        cerr << "input file argument missing, use the -i or --file flags." << endl;
        exit(0);
    }

    if (specCheck) {
        if (funcName.empty()) {
            cerr << "function name is missing, default is the first function in the file." << endl;
        }
        if (specName.empty()) {
            cerr << "specification name is missing, default is the first specification in the function." << endl;
        }
        cout << "running specCheck with file: " << inputFile << " function '" << funcName <<"', and specification '" << specName << "'." << endl;
        return specCheckMain(inputFile, funcName, specName);
    }

    if (smt) {
        cout << "translating to SMT and calling Z3 with file: " << inputFile << "." << endl;
        testMiniZ3(inputFile);
        return 0;
    }

    if (abc) {
        cout << "translating to Sequential Circit and calling ABC with file: " << inputFile << "." << endl;
        ABCMain(inputFile, funcName, (unsigned int)(bound), (unsigned int)(array_bound), abc_debug);
        return 0;
    }

    if (abc_debug) {
        cout << "translating to Sequential Circit and calling ABC with file: " << inputFile << "." << endl;
        ABCMain(inputFile, funcName, (unsigned int)(bound),4, abc_debug);
        return 0;
    }

    return cg2scMain(argc, argv);
}
